/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.Collection;

import org.eclipse.core.resources.IMarker;
import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.ConstructorInvocation;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.IMethodBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.SuperConstructorInvocation;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclaration;

import com.googlecode.syper.javasyp.checker.ExpressionEncoder.Lookup;
import com.googlecode.syper.javasyp.formulae.Formula;

/**
 * @author kevin
 *
 */
public interface IChecker {

	/**
	 * Error category for {@link IChecker#reportUserProblem(String, ASTNode, Category).
	 * @author kevin
	 */
	public enum Category {
		/** Required permissions */
		PRE(IMarker.SEVERITY_WARNING),
		/** Ensured permissions */
		POST(IMarker.SEVERITY_WARNING),
		/** Permissions for locals */
		LOCALS(IMarker.SEVERITY_WARNING),
		/** Specification syntax errors */
		SYNTAX(IMarker.SEVERITY_ERROR),
		/** Unsupported code patterns */
		UNSUPPORTED(IMarker.SEVERITY_INFO),
		/** Exposure error */
		EXPOSURE(IMarker.SEVERITY_WARNING),
		/** Logical error */
		PROVER(IMarker.SEVERITY_WARNING),
		/** Information to display to user */
		WARN(IMarker.SEVERITY_INFO);

		/** Eclipse marker {@link IMarker#SEVERITY severity} */
		public final int severity;

		private Category(int severity) { this.severity = severity; }
	}

	boolean isCancelable();
	boolean isCanceled();
	void cancel();

	/** Use this for instance methods <b>only</b> */
	RefType getReceiverType(IMethodBinding binding);

	/** Use this for constructors and methods */
	RefType getReturnType(IMethodBinding binding);

	/** Use this for constructors and methods */
	RefType getParamType(IMethodBinding binding, int paramIndex);

	/** Use this for locals including parameters */
	RefType getLocalType(VariableDeclaration declaration);

	/** Use this for fields and local variables */
	RefType getVariableType(IVariableBinding binding);

	/**
	 * Indicate that the running of this analysis on this compilation unit has created a problem.
	 *
	 * @param problemDescription
	 *            A textual description of the problem.
	 * @param node
	 *            The AST node where the problem was encountered.
	 * @param category
	 *            Problem category
	 */
	public void reportUserProblem(String problemDescription, ASTNode node, Category category);

	/*
	 * Contract methods for the various invocation nodes
	 */
	public abstract Contract getContract(SuperMethodInvocation node);

	public abstract Contract getContract(SuperConstructorInvocation node);

	public abstract Contract getContract(MethodInvocation node);

	public abstract Contract getContract(ConstructorInvocation node);

	public abstract Contract getContract(ClassInstanceCreation node);

	public abstract Contract getContract(MethodDeclaration node);

	public abstract Boolean getNullChecksFlag(IBinding binding);

	public abstract Boolean getBoundsChecksFlag(IBinding binding);

	/**
	 * Encodes the given expression as a formula using the given lookup callback
	 * @param e
	 * @param lookup
	 * @param preLookup pre-image lookup, which should usually simply return
	 * the first "incarnation" of a given reference, for encoding {@code \old}
	 * @return the given expression as a formula
	 * @see ExpressionEncoder#encode(Expression, Lookup)
	 */
	public Formula encode(Expression e, Lookup lookup, Lookup preLookup);

	/**
	 * Returns the loop invariant declared for the given loop body
	 * (statement or block), if any
	 * @param loopBody must not be {@code null}
	 * @return the loop invariant expressions declared in the given loop body, possibly empty
	 */
	public Collection<Expression> getLoopInvariant(Statement loopBody);

	/**
	 * Returns the class invariants declared for the given type node,
	 * including (visible) invariants declared in super-types
	 * @param type should not be {@code null}
	 * @return the visible object invariants declared for the given type
	 */
	public Collection<Expression> getInvariants(TypeDeclaration type);

	/**
	 * Returns the class invariants declared for the given type binding,
	 * including (visible) invariants declared in super-types
	 * @param type should not be {@code null}
	 * @return the visible object invariants declared for the given type
	 */
	public Collection<Expression> getInvariants(ITypeBinding type);
}
